\begin{tabbing}
$\forall$\=$D$:Dsys, $i$:Id, $s_{1}$, $s_{2}$:M($i$).state, $k_{1}$, $k_{2}$:Knd, $v_{1}$:d{-}decl($D$;$i$)($k_{1}$), $v_{2}$:d{-}decl($D$;$i$)($k_{2}$), $m_{1}$,\+
\\[0ex]$m_{2}$:\{$m$:M($i$).Msg$\mid$ source(mlnk($m$)) $=$ $i$ \} List.
\-\\[0ex]$\langle$$s_{1}$$,\,$doact($k_{1}$;$v_{1}$)$,\,$$m_{1}$$\rangle$ $=$ $\langle$$s_{2}$$,\,$doact($k_{2}$;$v_{2}$)$,\,$$m_{2}$$\rangle$ $\in$ d{-}world{-}state($D$;$i$)
\\[0ex]$\Rightarrow$ $s_{1}$ $=$ $s_{2}$ \& $k_{1}$ $=$ $k_{2}$ \& $v_{1}$ $=$ $v_{2}$ $\in$ d{-}decl($D$;$i$)($k_{1}$) \& $m_{1}$ $=$ $m_{2}$
\end{tabbing}